…d goto reduction (which needs to be checked again)

…tos)

…ameter

# Conflicts:
#	BoogieLang/Semantics.thy

simplify proofs in the process

… account

…ust_interface

…undational_boogie into adjust_interface

…undational_boogie into adjust_interface

…izations

should rename WhileWrapper eventually to something like "Boundary"

This helper lemma is used in cases when the loop head set representation
is different in a proof goal and in a lemma. Previously, the simplifier
was used on the proof goal, but the result does not always match the
representation of the lemma that is then applied. Now, the helper lemma
is applied instead.

…ion.thy (validation)